Consider the TRS R consisting of the rewrite rules
1:
if(true,x,y)
→ x
2:
if(false,x,y)
→ y
3:
if(x,y,y)
→ y
4:
if(if(x,y,z),u,v)
→ if(x,if(y,u,v),if(z,u,v))
There are 3 dependency pairs:
5:
IF(if(x,y,z),u,v)
→ IF(x,if(y,u,v),if(z,u,v))
6:
IF(if(x,y,z),u,v)
→ IF(y,u,v)
7:
IF(if(x,y,z),u,v)
→ IF(z,u,v)
Consider the SCC {5-7}.
By taking the AF π with
π(IF) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {1-7}
are strictly decreasing.
Hence the TRS is terminating.
Tyrolean Termination Tool (0.03 seconds)
--- May 3, 2006